Definition

Denote by 𝚂𝙰𝚃\mathtt{SAT} the set of all satisfiable CNF formulae.

(satisfiable meaning there is some assignment of variables such that the formula evaluates to TRUE)

Notes

  • 𝚂𝙰𝚃∈𝐍𝐏\mathtt{SAT} \in \mathbf{NP} (see NP)
    • as a proof of satisfiability may simply be a satisfying truth assignment
    • however, not clear for formulas not in SAT, what a proof of unsatisfiability could be, answer could yield insight on NP =? coNP (unresolved)
  • 𝚂𝙰𝚃\mathtt{SAT} is NP-hard
  • Cook-Levin theorem states that 𝚂𝙰𝚃\mathtt{SAT} is NP-complete
    • k-SAT is NP-complete for all k≥3k\geq 3
    • however, 2SAT can be solved in O(n+m)O(n+m) for nn variables, mm clauses
  • 𝚂𝙰𝚃≤p\mathtt{SAT} \leq_p 3SAT (reduces in polynomial time)
  • By Fagin's theorem, ESO = NP, thus SAT may be represented by ESO
    • ∃\exists (variables) such that CNF statement = true

References

  1. S. Arora, B. Barak. Computational Complexity: A Modern Approach, Cambridge University Press, 2009, p. 45.
  2. https://webdocs.cs.ualberta.ca/~zacharyf/courses/complexity_2019/notes/complexity-w19-lec04.pdf
  3. https://imangodoc.com/1SPxYenE.html
  4. https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
  5. https://people.csail.mit.edu/virgi/6.1420/lecture1.pdf
  6. https://mathweb.ucsd.edu/~sbuss/CourseWeb/Math268_2014W/Beame_IAS_proofcomplexity.pdf